refactor(Topology/Sion): use a dense and continuous completion to generalize the statements#38190
Conversation
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
…hlib4 into ACL/DedekindCut
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
AntoineChambert-Loir
changed the title
PR summary 885827f111
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Sion | 1451 | 1448 | -3 (-0.21%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Topology.Sion |
-3 |
Mathlib.Topology.Order.Completion (new file) |
859 |
Declarations diff
+ DedekindCut.continuous_principal
+ Fill
+ continuous_some
+ exists_dense_continuous_completion
+ exists_lt_iInf_of_lt_iInf_of_sup'
+ instance : DenselyOrdered (Fill α)
+ instance : TopologicalSpace (Fill α) := Preorder.topology _
+ instance [DenselyOrdered α] : DenselyOrdered (DedekindCut α)
+ instance [Preorder α] [Preorder β] [NoMaxOrder β] [DenselyOrdered β] :
+ instance [Preorder α] [Preorder β] [NoMinOrder β] [DenselyOrdered β] :
+ instance [TopologicalSpace α] [OrderTopology α] : OrderTopology (Fill α)
+ le_principal_iff
+ lt_iff_exists
+ lt_iff_exists'
+ lt_principal_iff
+ principal_le_iff
+ principal_lt_iff
+ some
- DMCompletion.exists_isSaddlePointOn
- exists_isSaddlePointOn'
- exists_saddlePointOn'
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com> Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
2 participants
Use the existence of a dense and continuous completion to simplify the final part of the proof of Sion's theorem.
As a matter of fact, only an early lemma needs to be modified and the rest holds in weaker assumptions,
leading to a serious simplification.
Since the PR proving Sion is very recent and unused, we didn't add deprecation lemmas.